(set-logic QF_LIA)
(set-option :proof true)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v12 Bool)
(declare-const i1 Int)
(declare-const i2 Int)
(declare-const i4 Int)
(declare-const i8 Int)
(declare-const i10 Int)
(declare-const v15 Bool)
(declare-const i15 Int)
(declare-const v18 Bool)
(declare-const v19 Bool)
(assert-soft (or (distinct v10 v8 (= v12 v10 v4 v8 (>= 57 i8) v0 v8 v6 v9 v15 v8) v9 (> i4 57)) v19))
(assert (or v18 v19 v6 (= v12 v10 v4 v8 (>= 57 i8) v0 v8 v6 v9 v15 v8) (=> v6 (> i4 57)) v6 (distinct i1 (- i15 72 33 i15 i2))))
(assert-soft (or (> i15 81) (distinct 57 i10)))
(assert (or v15 (> i15 81)))
(assert (or v7 v6))
(assert-soft (or v3 (=> v6 (> i4 57))))
(assert (or (=> v6 (> i4 57)) v1 v10 (<= 9 32)))
(assert-soft (or v18 (<= i1 71) (distinct 57 i10) (distinct 71 i1)))
(assert (or (= v12 v10 v4 v8 (>= 57 i8) v0 v8 v6 v9 v15 v8)))
(assert (or v6))
(assert (or (distinct v10 v8 (= v12 v10 v4 v8 (>= 57 i8) v0 v8 v6 v9 v15 v8) v9 (> i4 57)) (= v12 v10 v4 v8 (>= 57 i8) v0 v8 v6 v9 v15 v8) (<= 9 32) v19 (distinct i1 (- i15 72 33 i15 i2)) v7))
(check-sat)